the_w:World, e:E, t, t':.
FairFifo
 (isrcv(kind(e)))
 (match(lnk(kind(e));t;time(e)))
 (match(lnk(kind(e));t';time(e)))
 (t = t'  ) 

latex

Definitions

time(e), kind(e), lnk(k), match(l;t;t'), b, A, P  Q, a < b, isrcv(k), FairFifo, , x:A. B(x), E, World, x:A  B(x), P & Q, t  T, x:AB(x), P  Q, False, {x:A| B(x)} , , Void, A  B, , i  j , snds(l;t), ||as||, source(l), m(i;t), onlnk(l;mss), n+m, upto(n), Type, #$n, {i..j}, S  T, i  j < k, suptype(S; T), map(f;as), concat(ll), <a, b>, w.M, mlnk(m), Id, Msg(M), m(l;t), f(a), Msg, type List, s = t, x.A(x), True, T, P  Q, as @ bs, left + right, P  Q, Dec(P)

Lemmas

decidable lt, concat map upto, iseg length, append wf, squash wf, true wf, length append, w-onlnk wf, w-m wf, Msg wf, Id wf, mlnk wf, w-M wf, lsrc wf, length wf1, concat wf, map wf, le wf, int seg wf, w-Msg wf, upto wf, isrcv wf, fair-fifo wf, nat wf, w-E wf, world wf, assert wf, w-match wf, assert-w-match, lnk wf, w-ekind wf, w-time wf